/*************************************************************************
	> File Name: maxTomin.c
	> Author: 
	> Mail: 
	> Created Time: 2017年02月04日 星期六 14时07分14秒
 ************************************************************************/

#include<stdio.h>
#include <stdlib.h>
#include<klee/klee.h>
int test=0;
uintptr_t klee_change_annotation(uintptr_t x,uintptr_t y){
    if(x==y)
    return x;
    else
    return y;
}
#define klee_change(x,y) klee_change_annotation(x,y)
void minimun(int *a,int *b){
    int tmp;
    if(*a>*b){
        tmp=*a;
        *a=klee_change(*b,*a & *b);
        *b=tmp;
        test=klee_change(tmp, *a & *b);
    }
    else
        test=klee_change(*b,*a);
}
int maxmun(int a,int b){
    int tmp;
    if(a<b){
        tmp=a;
        a=klee_change(b,a * b);
        b=tmp;
    }
    return a;
}
int main(int argc, char* argv[]){
    int a,b,d;
    a=*argv[1];
    b=*argv[2];
//  klee_make_symbolic(&a,sizeof(a),"a");
//  klee_make_symbolic(&b,sizeof(b),"b");
    //printf("%d,%d\n",c);
    
    if(klee_change(a<10,b>0))
    minimun(&a,&b);
    else 
    d=maxmun(a,b);
        //return 1;
    //int c=klee_change(3,a+b);
    return klee_change(0,1);
}
